\begin{tabbing}
prod{-}deq($A$;$B$;$a$;$b$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\lambda$$A$,$B$,$a$,$b$,$p$,$q$. $q$/$q_{1}$,$q_{2}$.\+\+
\\[0ex]$p$/$p_{1}$,$p_{2}$.
\\[0ex]$b$/${\it eq}$,$b_{1}$.
\\[0ex]$a$/$e_{1}$,$a_{1}$.
\\[0ex]($\lambda$$\%_{1}$.\=$\%_{1}$\+
\\[0ex](\=$\langle$$\lambda$$\%$.\=$\langle$($\lambda$$\%_{1}$.$\%_{1}$($p_{1}$,$q_{1}$)/$\%_{4}$,$\%_{5}$. $\%_{4}$(($\lambda$$\%_{1}$.$\%_{1}$)(($\lambda$$\%_{1}$.$\ast$)($\ast$))))($a_{1}$)\+\+
\\[0ex]$,\,$($\lambda$$\%_{1}$.$\%_{1}$($p_{2}$,$q_{2}$)/$\%_{4}$,$\%_{5}$. $\%_{4}$(($\lambda$$\%_{1}$.$\%_{1}$)(($\lambda$$\%_{1}$.$\ast$)($\ast$))))($b_{1}$)$\rangle$
\-\\[0ex]$,\,$$\lambda$$\%$.$\%$/$\%_{1}$,$\%_{2}$. $\ast$$\rangle$))
\-\-\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$/$\%_{2}$,$\%_{3}$. $\%_{3}$)\+
\\[0ex](\=($\lambda$$\%_{1}$.\=$\%_{1}$\+\+
\\[0ex]($\langle$$p_{1}$$,\,$$p_{2}$$\rangle$ $=$ $\langle$$q_{1}$$,\,$$q_{2}$$\rangle$
\\[0ex],$\langle$$p_{1}$$,\,$$p_{2}$$\rangle$ $=$ $\langle$$q_{1}$$,\,$$q_{2}$$\rangle$
\\[0ex],$e_{1}$($p_{1}$,$q_{1}$) $\wedge_{2}$ ${\it eq}$($p_{2}$,$q_{2}$)
\\[0ex],$e_{1}$($p_{1}$,$q_{1}$) \& ${\it eq}$($p_{2}$,$q_{2}$)
\\[0ex],($\lambda$$\%_{1}$.$\%_{1}$)(($\lambda$$\%_{1}$.$\langle$$\lambda$$\%_{2}$.$\%_{2}$$,\,$$\lambda$$\%_{2}$.$\%_{2}$$\rangle$)($\ast$))
\\[0ex],\=($\lambda$$\%_{1}$.$\%_{1}$)\+
\\[0ex](\=($\lambda$$\%_{1}$.$\%_{1}$($e_{1}$($p_{1}$,$q_{1}$),${\it eq}$($p_{2}$,$q_{2}$)))\+
\\[0ex]($\lambda$$p$,$q$. \=Case $q$ of\+
\\[0ex]inl($x$) $\Rightarrow$ \=Case $p$ of\+
\\[0ex]inl($x$) $\Rightarrow$ $\langle$$\lambda$$\%$.$\langle$$\ast$$,\,$$\ast$$\rangle$$,\,$$\lambda$$\%$.$\ast$$\rangle$
\\[0ex]inr($y$) $\Rightarrow$ $\langle$$\lambda$$\%$.$\langle$any($\%$)$,\,$$\ast$$\rangle$$,\,$$\lambda$$\%$.$\%$/$\%_{1}$,$\%_{2}$. any($\%_{1}$)$\rangle$
\-\\[0ex]inr($y$) $\Rightarrow$ \=Case $p$ of\+
\\[0ex]inl($x$) $\Rightarrow$ $\langle$$\lambda$$\%$.$\langle$$\ast$$,\,$any($\%$)$\rangle$$,\,$$\lambda$$\%$.$\%$/$\%_{1}$,$\%_{2}$. any($\%_{2}$)$\rangle$
\\[0ex]inr($y$) $\Rightarrow$ $\langle$$\lambda$$\%$.$\langle$any($\%$)$,\,$any($\%$)$\rangle$$,\,$$\lambda$$\%$.$\%$/$\%_{1}$,$\%_{2}$. any($\%_{2}$)$\rangle$))))
\-\-\-\-\-\\[0ex]($\lambda$$P_{1}$,$P_{2}$,$Q_{1}$,$Q_{2}$,$\%$,$\%_{1}$. \=$\langle$$\lambda$$\%_{2}$.\=$\langle$$\lambda$$\%_{3}$.\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+\+\+
\\[0ex]$\%_{5}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{5}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$. $\%_{6}$(($\lambda$$\%_{4}$.$\%_{4}$)(($\lambda$$\%_{4}$.$\%_{4}$)($\%_{3}$))))\+
\\[0ex]($\%$))))
\-\-\-\\[0ex]($\%_{2}$))))
\-\-\-\\[0ex]($\%_{1}$)
\-\\[0ex]$,\,$$\lambda$$\%_{3}$.\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{5}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{6}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$. $\%_{6}$(($\lambda$$\%_{4}$.$\%_{4}$)(($\lambda$$\%_{4}$.$\%_{4}$)($\%_{3}$))))\+
\\[0ex]($\%_{1}$))))
\-\-\-\\[0ex]($\%_{2}$))))
\-\-\-\\[0ex]($\%$)$\rangle$
\-\-\\[0ex]$,\,$$\lambda$$\%_{2}$.\=$\langle$$\lambda$$\%_{3}$.\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+\+
\\[0ex]$\%_{6}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{5}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$. $\%_{5}$(($\lambda$$\%_{4}$.$\%_{4}$)(($\lambda$$\%_{4}$.$\%_{4}$)($\%_{3}$))))\+
\\[0ex]($\%$))))
\-\-\-\\[0ex]($\%_{2}$))))
\-\-\-\\[0ex]($\%_{1}$)
\-\\[0ex]$,\,$$\lambda$$\%_{3}$.\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{6}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=(\=$\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$.\+\+
\\[0ex]$\%_{6}$
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$)\+
\\[0ex](\=($\lambda$$\%_{4}$.$\%_{4}$/$\%_{5}$,$\%_{6}$. $\%_{5}$(($\lambda$$\%_{4}$.$\%_{4}$)(($\lambda$$\%_{4}$.$\%_{4}$)($\%_{3}$))))\+
\\[0ex]($\%_{1}$))))
\-\-\-\\[0ex]($\%_{2}$))))
\-\-\-\\[0ex]($\%$)$\rangle$$\rangle$))))
\-\-\-\-\-\-\\[0ex]($A$
\\[0ex],$B$
\\[0ex],$a$
\\[0ex],$b$)
\-
\end{tabbing}